@${\it loc}$: $k$ writes only members of $L$
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$inr(inr(inr(inr(inr(inr(inr(inr(inl($\langle$${\it loc}$$,\,$$k$$,\,$$L$$\rangle$)))))))))